\documentclass[10pt]{article}

\usepackage{enumerate}
\usepackage[english]{babel}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{graphicx}

\title{Software Security Lab 1}
\author{David Falk dfa@kth.se \\ Marcus Öberg marcusob@kth.se}

\begin{document}
\maketitle
\section*{Tasks}
\subsection*{Task 1}
\begin{enumerate}[(a)]
\item Explain the behaviours of the Bidder and the Auctioneer.

At initialization the clients bid is chosen by a if statement. Then the auctioneer is started. From the auctioneer the client is run and the client waits for the auctioneer to start the auction. The auctioneer waits for a start auction message that init sends. When the auctioneer has recieved the start auction message it sends a auction started message to the client and waits for a bid to be submitted. When the client recieves the auction started message it sends the bid calculated at init then waits for a result. The auctioneer recieves the bid from the client and calculates the result and sends it to the client. The client recieves the result and prints if it won or lost. The client waits for auction close and the auctioneer sends auction close. Then both the client and the auctioneer closes.

Client does not specifically wait for a end auction message it could be a start auction message. This is however not an issue because the auctioneer can only send an end auction in that state.

\includegraphics[scale=0.75]{4_1_a.png}

\item Do you get any errors while verifying with default options of spin? If
yes, explain the error trace and do the modifications needed to fix it.

Yes, error client waits for data available in channel \texttt{m2B} (line 61 - 68) and the auctioneer doesn't get a match for the if condition (line 92 -95) because there is no guard for when the startbid is equal to the placed bid.

\textbf{Modification:} Change condition on line 93 to \texttt{clientBid >= startBid}.

\item \label{4_c} Specify the following properties in LTL. Motivate your answer.

Because the channels \texttt{m2A} and \texttt{m2B} are rendezvous channels (no buffer) it is not possible to read from these in the ltl-formula. We believe this is due to the fact that these channels require a handshake. The third property require a distinction between not won and lost.

\textbf{Modifications:} We added \texttt{lost} and\texttt{won} to \texttt{mtype} for \texttt{Bidder1 States} and \texttt{stateWinner} as a variable with mtype. \texttt{stateWinner} is set to \texttt{won} or \texttt{lost} depending on the outcome of the auction in reference to the bidder. This was adequate to take care of the issues above.

\begin{enumerate}[i.]
\item \textit{If Bidder’s bid is greater than Auctioneer’s initial bid, Bidder wins at some point in the future.}\label{first_ltl}

\texttt{ltl i \{(clientBid>startBid) -> <>(stateWinner==won)\}}
\\[2mm]
This says that if clientBid is bigger than startbid then it implies that statewinner will be won at some point in the future. This only tests the first condition in the starting state. The condition is false in the starting case because clientBid is inialized to zero.

\item \textit{Always, if Bidder’s bid is greater than Auctioneer’s initial bid, Bidder wins at some point in the future.}

\texttt{ltl ii \{[]((clientBid>startBid) -> <>(stateWinner==won))\}}
\\[2mm]
This says that for all states it is true that if \texttt{clientBid} is bigger than \texttt{startBid} then it is implied that \texttt{stateWinner} will be won at some point in the future. This holds since the whole statement is true even when the first condition is false.

\item \textit{Always, eventually Bidder either wins or loses.}

\texttt{ltl iii \{ []<>(stateWinner==won || stateWinner==lost) \}}
\\[2mm]
In every state it is true that there exists a future state where stateWinner is either won or lost. It is however not the same as: in every state there exists a future state where stateWinner is either won or not won. This is because when the auction is ongoing the clients have not lost. 

\end{enumerate}

\item Check the above properties with spin and explain your results. Here
and in the following tasks, in the case a property does not hold,
describe an error scenario based on the counterexample provided by
spin.

\begin{enumerate}[i.]

\item We do not get any errors when testing the first ltl-formula in spin. However nothing valuable is tested. This is, as stated above, due to the initialization of clientBid to zero. Which means that the first condition is false in the first state and therefore the whole statement holds. The result from spin tells us that most of the states are not tested.

To change this to a meaningfull test we chose to add eventually in front of the first statement. This means that when clientBid is larger than startBid then the client will win in some point in the future.

\texttt{ltl i \{<>(clientBid>startBid) -> <>(stateWinner==won)\}}

\item We do not get any errors when testing the second ltl-formula in spin. We also reach all states in the model so the statement holds in the whole model. 
    
\item Same as above
\end{enumerate}

\end{enumerate}

\subsection*{Task 2}
We extended the \textsc{promela} model to handle $n$ clients.

\textbf{Assumptions} \\
\begin{description}
\item[\textbf{nrounds:}] We don't force the clients to give up but sets the winner to the client with max bid after the $n$ rounds. The clients do however give up if current max bid is higher than the clients bid limit.

\item[\textbf{Current winner:}] We assume that the client who currently has the winning bid does not wish to place a higher bid, and subsequently the auctioneer will never ask this client to place a bid.

\item[\textbf{Manner of bidding:}] To simplify the bidding process we chose to let the auctioneer ask each client in turn if it wants to place a bid.

%\item[\textbf{Manner of}] To simplify the bidding process we chose to let the auctioneer ask each
%\vspace{-10pt}\item[\textbf{bidding}] client in turn if it wants to place a bid.

\end{description}


\noindent \textbf{Description}
\\
\\
We changed the channel $m2B$ to an array of channels, one for each client. The auctioneer uses these channels to send messages to a specific client. We replaced $lost$ and $won$ from mtype that we had created in task 1 with the message $loser$ that the auctioneer sends (the message $winner$ already existed). The events $send\_bid$ and $danger$ were added to mtype. $send\_bid$ is used when the auctioneer asks a client to send a bid and $danger$ is used to stop the auction prematurely.

To keep track of the clients who have given up we created an array $gUp$ that denotes which clients have given up. To avoid iterating through the list to calculate the amount of users that have given up we also created a variable $amountGivenUp$. When we extended the model to handle more than one client we needed to set individual bids for each client and the logical way was to change the variable $client\_bid$ so it is a local variable in the proctype client.
\\ \\
\textbf{Init:} Init starts all the clients within a loop that runs $n$ times. It sends an id to each client that is indexed to zero. After all clients are created the auctioneer is run. Before init terminates it sends the $start\_auction$ message.
\\ \\
\textbf{Client:} The client chooses a bid limit then waits for auction to start. When the auction has started the client waits for the auctioneer to ask it to place a bid. When the actioneer asks the client to send a bid it includes the current max bid. The client calculates a bid that is max bid + [1-5]. If this bid is higher than its bid limit then the bid is not sent to the auctioneer and instead sends zero as the bid which indicates that the client gives up. When the client gives up it also sets its value in $gUp$ to true. If the client does not want to give up the bid is sent to the auctioneer. If the client has given up the auctioneer will send a loser message and the client will wait for the $end\_auction$ signal. If the client has chosen to continue the process above is repeated until the auctioneer choses a winner.
\\ \\
\textbf{Auctioneer:} The auctioneer waits to recieve the $start\_auction$ message from init. When this has been recieved the $auction\_started$ message is sent to all clients. Then it will ask each client, that has not given up, in turn to send a bid. The $send\_bid$ message contains the current $max\_bid$. If the recieved bid is zero, the client has chosen to give up and then the auctioneer send a $loser$ message to the client. Otherwise the bid will be stored as the current $max\_bid$ and the next client will be asked to place a bid. This is repeated until either only one client remains in the auction or until the max number of rounds has been reached. At this point the auctioneer send a $winner$ message to the client who currently has the $max\_bid$ and sends a $loser$ message to all other clients who still remains in the auction. The $end\_auction$ message is now sent to all clients and the auctioneer terminates.
\\ \\
\noindent \textbf{LTL-formulas}

\noindent \texttt{ltl i \{[]<> someoneWon\}} \\
\noindent \texttt{ltl ii \{[] ((bids[0] > bids[1]) -> (<> (someoneWon \&\& max$\_$id==0)))\}} \\
\noindent \texttt{ltl iii1 \{!someoneWon U (amountGivenUp==1)\}} \\
\noindent \texttt{ltl iii2 \{!someoneWon U (amountGivenUp==(amountOfClients-1))\}} \\
\noindent \texttt{ltl iv \{[](!dang -> (<> (someoneWon \&\& (max\_id==0 || max\_id==1)))\}} \\


\subsection*{Task 3}
We have chosen to implement the japanese auctioning protocol.
\\ \\
\textbf{Assumptions}
\begin{description}
\item[\textbf{Tie:}] We have assumed that if two or more clients submit the same bid and no one wishes to place a higher bid no client wins.
\end{description}

\noindent \textbf{Description} \\
The program flow is similar to the protocol described above with some differences. These are:

\begin{description}
\item[\textbf{Current bid:}] The clients no longer places a bid, instead the auctioneer increases the current bid at the beginning of each round and then asks each client if it wants to accept the current bid.

\item[\textbf{nround:}] The number of rounds is not limited. The current bid will increase until only one or no client still remain.
 
\end{description}

\noindent \textbf{LTL-formulas}

\noindent \texttt{ltl   i \{[]<> (amountGivenUp > (amountOfClients-2))\}} \\
\noindent \texttt{ltl  ii \{[]<> (someoneWon || amountGivenUp==amountOfClients)\}} \\
\noindent \texttt{ltl iii \{!someoneWon U (amountGivenUp > amountOfClients-2)\}} \\


\subsection*{Task 4}
We have chosen to implement the First-price sealed-bid.
\textbf{Assumptions}
\begin{enumerate}
\item[\textbf{Tie:}] We have assumed that if two or more clients submit the same bid and it is the highest bid no client wins.
\end{enumerate}
\noindent \textbf{Description} \\
The program flow is similar to the protocol described above with some differences. These are:

\begin{description}
\item[\textbf{Current bid:}] The clients will send one bid each. The client with the highest bid after one round wins.

\item[\textbf{nround:}] Only one round.
 
\end{description}

\noindent \textbf{LTL-formulas}

\noindent \texttt{ltl   i \{[] (round<2) \}} \\
\noindent \texttt{ltl  ii \{!someoneWon U (amountOfBids == amountOfClients)\}} \\
\noindent \texttt{ltl iii \{[] (amountOfBids<amountOfClients -> !someoneWon)\}}


\end{document}